w:World, p:FairFifo, e:E, l:IdLnk. w_sends(e;l)  Msg List 

latex

Definitions

t  T, x:A. B(x), <a,b>, IdLnk, x:AB(x), True, T, tag(k), lnk(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), rcv(l,tg), Prop, b, A, Void, x:AB(x), A & B, SWellFounded(R(x;y)), P  Q, False, P & Q, EOrderAxioms(E; pred?; info), e < e', left+right, x:A. B(x), P  Q, FairFifo, World, kind(e), loc(e), time(e), Knd, strong-subtype(A;B), x. t(x), 2of(t), a(i;t), isnull(a), {x:A| B(x) }, EqDecider(T), w_sends(e;l), Msg, type List, w.M, f(a), x.A(x), Msg(M), Type, s = t, w-order-axioms, 1of(t), val(e), w-info(w;e), w-pred(w;e), V(i;k), IdLnkDeq, NatDeq, IdDeq, , Id, product-deq(A;B;a;b), E, a<b, pred(e), first(e)

Lemmas

first wf, pred wf, w-time wf, w-pred-decreases, sends wf, product-deq wf, id-deq wf, nat-deq wf, strong-subtype-deq-subtype, strong-subtype-set3, not wf, assert wf, w-isnull wf, w-a wf, pi1 wf, pi2 wf, strong-subtype-self, nat wf, idlnk-deq wf, Knd wf, w-eval wf, w-loc-lemma, w-kind-lemma, subtype rel self, w-V wf, w-loc wf, w-ekind wf, w-order-axioms, world wf, fair-fifo wf, EOrderAxioms wf, w-pred wf, w-info wf, w-E wf, Msg wf, squash wf, true wf, IdLnk wf, Id wf, w-M wf